Summary

This PR records a single TODO item in
Physlib/Particles/StandardModel/HiggsBoson/EffectivePotential.lean.

The TODO was human-written; Claude placed it in the appropriate file and
section of the library and verified that the build and linters remain green.

Original user input

change the Polynomial in Effective Potential for the Higgs field to be based
on the basis independent Module.Dual HiggsVec R, rather then on Fin 4.

What was added

A TODO command just after apply_eq_polynomial, inside section B. Maximum
mass dimension, next to the declarations it concerns (HasMaxMassDimLE and
polynomial):

TODO "Reformulate `HasMaxMassDimLE` (and `polynomial`) to use the basis-independent polynomial
  ring `MvPolynomial (Module.Dual ℝ HiggsVec) ℝ` rather than `MvPolynomial (Fin 4) ℝ`, so that the
  effective potential is expressed without reference to the explicit coordinate map
  `HiggsVec.toRealScalars`."

Why this is the right home

HasMaxMassDimLE and polynomial currently express the effective potential as
an MvPolynomial (Fin 4) ℝ evaluated on HiggsVec.toRealScalars, i.e. tied to
an explicit coordinate choice. The TODO sits directly beside these definitions,
making the intended basis-independent reformulation discoverable to future
contributors. No TODO for this already existed.

Verification

• lake build succeeds with the TODO elaborating cleanly (no sorry, no new
  axioms, no new warnings).
• lake exe runPhyslibLinters passes.
• ./scripts/lint-style.sh passes.

Human review

• Does the TODO item look correctly placed in the library and an accurate reflection of the input? Yes